<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
<!-- saved from url=(0070)http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000756.html -->
<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
   <title> [klee-dev] How to get the path constrain in a readable way
   </title>
   <link rel="Index" href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/index.html">
   <link rel="made" href="mailto:klee-dev%40keeda.stanford.edu?Subject=Re:%20%5Bklee-dev%5D%20How%20to%20get%20the%20path%20constrain%20in%20a%20readable%20way&In-Reply-To=%3C4EB2C3CE.9070700%40imperial.ac.uk%3E">
   <meta name="robots" content="index,nofollow">
   
   <link rel="Previous" href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000755.html">
   <link rel="Next" href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000757.html">
 </head>
 <body bgcolor="#ffffff">
   <h1>[klee-dev] How to get the path constrain in a readable way</h1>
    <b>Cristian Cadar</b> 
    <a href="mailto:klee-dev%40keeda.stanford.edu?Subject=Re:%20%5Bklee-dev%5D%20How%20to%20get%20the%20path%20constrain%20in%20a%20readable%20way&In-Reply-To=%3C4EB2C3CE.9070700%40imperial.ac.uk%3E" title="[klee-dev] How to get the path constrain in a readable way">c.cadar at imperial.ac.uk
       </a><br>
    <i>Thu Nov  3 09:39:42 PDT 2011</i>
    <p></p><ul>
        <li>Previous message: <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000755.html">[klee-dev] How to get the path constrain in a readable way
</a></li>
        <li>Next message: <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000757.html">[klee-dev] bug in ObjectState::read?
</a></li>
         <li> <b>Messages sorted by:</b> 
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/date.html#756">[ date ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/thread.html#756">[ thread ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/subject.html#756">[ subject ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/author.html#756">[ author ]</a>
         </li>
       </ul>
    <hr>  
<!--beginarticle-->
<pre>Hi,

The STP input language used by the .cvc files is documented here:
<a href="http://sites.google.com/site/stpfastprover/stp-documentation">http://sites.google.com/site/stpfastprover/stp-documentation</a>

The PC language used by the .pc files is documented here:
<a href="http://klee.llvm.org/KQuery.html">http://klee.llvm.org/KQuery.html</a>

Best,
Cristian

On 03/11/11 15:00, amitaï madar wrote:
&gt;<i> Hi all.
</i>&gt;<i> I want to get the path constraints of each test case that KLEE creates
</i>&gt;<i> in a readable way.
</i>&gt;<i> for example with the following program:
</i>&gt;<i> int foo(int x) {    
</i>&gt;<i> if(x&gt;0)
</i>&gt;<i>        return 1;
</i>&gt;<i> return 0;
</i>&gt;<i>   } 
</i>&gt;<i> 
</i>&gt;<i>   int main() {
</i>&gt;<i>       int x;
</i>&gt;<i>       klee_make_symbolic(&amp;x, sizeof(x), "x");
</i>&gt;<i>       return foo(x);
</i>&gt;<i>   }
</i>&gt;<i> 
</i>&gt;<i> I want to get: 
</i>&gt;<i> -testcase000001.ktest is for x&gt;0
</i>&gt;<i> -testcase000002.ktest is for x&lt;0
</i>&gt;<i> I read on the archive that someone succeed this with the .cvc files.
</i>&gt;<i> However the .cvc files look like this 
</i>&gt;<i> __tmpInt8  : BITVECTOR(8);
</i>&gt;<i> __tmpInt16  : BITVECTOR(16);
</i>&gt;<i> __tmpInt32  : BITVECTOR(32);
</i>&gt;<i> __tmpInt64  : BITVECTOR(64);
</i>&gt;<i> x_0xa05ad38  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
</i>&gt;<i> %----------------------------------------------------
</i>&gt;<i> ASSERT( SBVLT(0hex00000000,(x_0xa05ad38[0hex00000003] @
</i>&gt;<i> (x_0xa05ad38[0hex00000002] @ (x_0xa05ad38[0hex00000001] @
</i>&gt;<i> x_0xa05ad38[0hex00000000])
</i>&gt;<i> )
</i>&gt;<i> )
</i>&gt;<i> )
</i>&gt;<i>  );
</i>&gt;<i> %----------------------------------------------------
</i>&gt;<i> QUERY( FALSE  );
</i>&gt;<i> I'm looking for a way to get from this  x&gt;0.
</i>&gt;<i> I tried to use STP constrain solver but was unsuccessful.
</i>&gt;<i> There is also .pc file that looks like this:
</i>&gt;<i> array x[4] : w32 -&gt; w8 = symbolic
</i>&gt;<i> (query [(Slt 0
</i>&gt;<i>              (ReadLSB w32 0 x))]
</i>&gt;<i>        false)
</i>&gt;<i> but again this isn't easily understandable.
</i>&gt;<i> Thanks for your help.
</i>&gt;<i> 
</i>&gt;<i> 
</i>&gt;<i> 
</i>&gt;<i> 
</i>&gt;<i> _______________________________________________
</i>&gt;<i> klee-dev mailing list
</i>&gt;<i> <a href="http://keeda.stanford.edu/mailman/listinfo/klee-dev">klee-dev at keeda.stanford.edu</a>
</i>&gt;<i> <a href="http://keeda.stanford.edu/mailman/listinfo/klee-dev">http://keeda.Stanford.EDU/mailman/listinfo/klee-dev</a>
</i>
</pre>

<!--endarticle-->
    <hr>
    <p></p><ul>
        <!--threads-->
	<li>Previous message: <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000755.html">[klee-dev] How to get the path constrain in a readable way
</a></li>
	<li>Next message: <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/000757.html">[klee-dev] bug in ObjectState::read?
</a></li>
         <li> <b>Messages sorted by:</b> 
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/date.html#756">[ date ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/thread.html#756">[ thread ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/subject.html#756">[ subject ]</a>
              <a href="http://keeda.stanford.edu/pipermail/klee-dev/2011-November/author.html#756">[ author ]</a>
         </li>
       </ul>

<hr>
<a href="http://keeda.stanford.edu/mailman/listinfo/klee-dev">More information about the klee-dev
mailing list</a><br>

</body></html>